
; Copyright (c) 2015 Microsoft Corporation
(set-option :auto-config true)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 11) (_ BitVec 9) (_ BitVec 15)) (_ BitVec 10))
(declare-fun p0 ( (_ BitVec 12) (_ BitVec 6)) Bool)
(declare-fun p1 ( (_ BitVec 15) (_ BitVec 15) (_ BitVec 1)) Bool)
(declare-fun v0 () (_ BitVec 7))
(assert (let ((e1(_ bv81 9)))
(let ((e2 (ite (bvsle e1 e1) (_ bv1 1) (_ bv0 1))))
(let ((e3 (f0 ((_ zero_extend 2) e1) ((_ sign_extend 8) e2) ((_ sign_extend 14) e2))))
(let ((e4 (ite (p0 ((_ sign_extend 5) v0) ((_ extract 7 2) e3)) (_ bv1 1) (_ bv0 1))))
(let ((e5 (bvsrem e3 e3)))
(let ((e6 (ite (p1 ((_ sign_extend 5) e5) ((_ zero_extend 6) e1) ((_ extract 8 8) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (p0 ((_ zero_extend 11) e2) ((_ sign_extend 5) e2))))
(let ((e8 (p1 ((_ zero_extend 14) e2) ((_ zero_extend 6) e1) ((_ extract 3 3) e3))))
(let ((e9 (bvule e3 e3)))
(let ((e10 (bvule e2 e4)))
(let ((e11 (bvule ((_ sign_extend 9) e2) e3)))
(let ((e12 (= ((_ zero_extend 9) e2) e3)))
(let ((e13 (distinct e5 ((_ sign_extend 3) v0))))
(let ((e14 (bvsge e3 ((_ zero_extend 1) e1))))
(let ((e15 (bvuge ((_ sign_extend 2) v0) e1)))
(let ((e16 (bvslt e6 e4)))
(let ((e17 (or e13 e15)))
(let ((e18 (xor e9 e16)))
(let ((e19 (=> e8 e10)))
(let ((e20 (xor e12 e18)))
(let ((e21 (and e11 e19)))
(let ((e22 (xor e20 e7)))
(let ((e23 (=> e14 e14)))
(let ((e24 (or e17 e21)))
(let ((e25 (ite e24 e22 e24)))
(let ((e26 (or e25 e25)))
(let ((e27 (and e26 e23)))
e27
))))))))))))))))))))))))))))
(check-sat)
